Feasible(M)
== xdom(1of(M)). T=1of(M)(x)   T
== & kdom(1of(2of(M))). T=1of(2of(M))(k)   Dec(T)
== & adom(1of(2of(2of(2of(M))))). 
== & p=1of(2of(2of(2of(M))))(a)   s:State(1of(M)). Dec(v:1of(2of(M))(locl(a))?Top. p(s,v))
== & xdom(1of(M)). T=1of(M)(x)   AtomFree(Type;T)
== & kdom(1of(2of(M))). T=1of(2of(M))(k)   AtomFree(Type;T)
== & ma-frame-compat(M;M) 

latex

---

clarification:

ma-feasible{i:l}
ma-feasible(M)
== fpf-all(Id; IdDeq; 1of(M); x,T.T)
== & fpf-all(Knd; KindDeq; 1of(2of(M)); k,T.Dec(T))
== & fpf-all(Id;
== & fpf-all(IdDeq;
== & fpf-all(1of(2of(2of(2of(M))));
== & fpf-all(a,p.(s:State(1of(M)). Dec(v:fpf-cap(1of(2of(M));KindDeq;locl(a);Top). p(s,v))))
== & fpf-all(Id; IdDeq; 1of(M); x,T.AtomFree(Type{i};T))
== & fpf-all(Knd; KindDeq; 1of(2of(M)); k,T.AtomFree(Type{i};T))
== & ma-frame-compat(M;M) 

latex

Definitions	x:A. B(x), State(ds), Dec(P), x:A. B(x), f(x)?z, locl(a), Top, f(a), P & Q, Id, IdDeq, xdom(f). v=f(x)   P(x;v), Knd, KindDeq, 1of(t), 2of(t), AtomFree(T;x), Type, ma-frame-compat(A;B)
FDL editor aliases	ma-feasible